$\forall$$A$:Type. safety($A$;$L$.no\_repeats($A$;$L$))